A:Type, l:(A List). (||l||  1 )  (||tl(l)|| = (||l|| - 1)) 

latex

Definitions	t  T, x:A. B(x), P  Q, False, Y, tl(l), ||as||, A, A  B, i  j ,
Lemmas	length wf2, ge wf, length wf1